1. Technical Field
The present invention relates to computer software, and more particularly to mining interface specifications using inductive logic to permit interfacing with different software programs and libraries.
2. Description of the Related Art
Software libraries are ubiquitous mechanisms for organizing widely useful functionalities to promote modularity and code reuse. A typical software library is used by client programs through an application program interface (API) with the library internals hidden from the client. Typically, the rules governing the correct usage of the API are documented informally. In many cases, libraries may have complex API usage rules and unclear documentation. As a result, the behavior of the library under some corner cases may not be well understood by the programmer. Therefore, obtaining formal specifications for such libraries is useful for software verification.
Software libraries are used frequently to promote modularity and code re-use. Common examples of libraries include operating system functionalities such as threads, files and sockets; data structure implementations such as stacks, queues, lists and hash tables; utilities for reading, writing and interpreting codecs; database processing and so on. The functionalities provided by a library are exported through an interface (API). Usage rules are formulated to govern the proper usage of an interface. These interface usage rules are usually a combination of two types of rules: (a) preconditions on the arguments of function calls and (b) admissible sequences of function calls to the API. Any violation of the API usage norms can lead to faulty or unpredictable behavior in programs.
In theory, the restrictions on the calls to an API can be formally specified along with the API. In practice, however, specifications of API behavior and restrictions on its usage are stated informally in a natural language. Such specifications may be ambiguous or even inaccurate. These specifications cannot therefore be used in verification systems. Often, informal specifications may not specify all the corner case behaviors. Existing verification tools such as SLAM™, Blast™, ESP™ and F-Soft™ can make use of formal specifications of valid/invalid usages of a given API, and automatically check application code for conformance. Such tools mostly rely on the user to provide specifications for the library APIs used by the application. The process of manually writing the specifications for APIs is cumbersome and prone to errors. Therefore, it is desirable to have automatic techniques to learn such specifications.
There are two types of approaches to learning specifications. The first type of approach starts by analyzing many trusted applications that use the library under consideration, whereas the second type of approach analyzes the library itself. Furthermore, approaches for inferring specifications may be static or dynamic. Static approaches analyze the source code to extract these specifications while dynamic approaches infer the required behavior by analyzing the runtime behavior. Finally, approaches may be geared towards different types of specifications of the API's behavior. Some techniques learn preconditions for function call parameters expressed in a suitable constraint language. Other techniques derive automata-based characterizations of legal/illegal calling sequences.